n:. r:. (((r * r)  n) & (n < ((r+1) * (r+1)))) 

latex

ProofTree

Definitions	s = t, t  T, , x:AB(x), A  B, a < b, x:A  B(x), P & Q, x:A. B(x), x:A. B(x), {x:A| B(x)} , i  j , P  Q, Void, False, A, #$n, -n, n+m, n - m, n * m, , , |g|, S  T, Type, left + right, P  Q, Dec(P), b, b | a, a ~ b, a  b, a <p b, a < b, A c B, f(a), x f y, xL. P(x), (xL.P(x))
Lemmas	decidable le, member wf, ge wf, nat properties, nat ind tp, le wf, nat wf